$\forall$${\it es}$:ES, $i$:Id, $P$:(state@$i$$\rightarrow$Prop).
\\[0ex]@$i$ stable ${\it state}$.$P$(${\it state}$)   $\Rightarrow$ $\forall$$e$@$i$. $P$((state when $e$)) $\Rightarrow$ $\forall$${\it e'}$$\geq$$e$.$P$((state when ${\it e'}$))